es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
es-triggers-params-consistent(es;A;i;ds;conds)
 (e:E.
 ((e  es-triggers(es;i;ds;conds)))
  (loc(e) = i & (kind(e)  fpf-domain(conds))
  & (isl((conds(kind(e)).2)((state when e),val(e)))))) 

latex

Definitions	x:A. B(x), P  Q, t  T, x. t(x), P & Q, A c B, , x:A. B(x), SQType(T), {T}, x(s), es-triggers-params-consistent(es;A;i;ds;conds)
Lemmas	es-E wf, es-triggers-params-consistent wf, fpf wf, Knd wf, decl-state wf, top wf, Id wf, event system wf, es-is-interface-triggers, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, es-kind wf, es-loc wf, Id sq